Hiroshi MATSUNO Chen LI Satoru MIYANO
Petri nets have recently become widely accepted as a description method for biological pathways by researchers in computer science as well as those in biology. This paper gives an overview of Petri net formalisms to describe biological pathways and discusses their use in modelings and simulations for the systematic understandings of biological pathways. After reviewing the use of various types of Petri nets for the biological pathway modelings, we showed the examples that analyze fundamental properties of biological pathways using T-invariant, P-invariant, siphon, and trap. Applications of hybrid Petri nets for producing new biological hypotheses through simulations are also illustrated.
Takashi ITO Susumu HASHIZUME Tomoyuki YAJIMA Katsuaki ONOGI
A batch process is a discontinuous and concurrent process which is suitable for multi-product, small-sized production. The distinctive feature of a batch process is that various decision making processes, such as scheduling, design, operation, etc. are strongly connected with each other. Interaction among these processes is necessary to dynamically and flexibly cope with a variety of unplanned events. This paper aims at presenting a batch scheduling technique based on Petri net models and showing the possibilities of integration between scheduling and design of batch processes. For this purpose, it first views the behavior of a batch operating system as a discrete event system and presents a Petri net model to be used for scheduling, design and operation. It next formulates batch scheduling problems based on Petri net partial languages, proposes their solution technique and last discusses the integration between scheduling and design of batch systems.
Satoshi TAOKA Masahiro YAMAUCHI Toshimasa WATANABE
The minimum initial marking problem MIM of Petri nets is described as follows: "Given a Petri net and a firing count vector X, find an initial marking M0, with the minimum total token number, for which there is a sequence δ of transitions such that each transition t appears exactly X(t) times in δ, the first transition is enabled at M0 and the rest can be fired one by one subsequently." This paper proposes two heuristic algorithms AAD and AMIM + and shows the following (1) and (2) through experimental results: (1) AAD is more capable than any other known algorithm; (2) AMIM + can produce M0, with a small number of tokens, even if other algorithms are too slow to compute M0 as the size of an input instance gets very large.
Toshiyuki MIYAMOTO Sadatoshi KUMAGAI
Petri nets are a well-known graphical and modeling tool for concurrent and distributed systems, and there have been many results on the theory, and also on practical applications. In the last decade, various Object-Oriented Petri nets (OO-nets) are proposed. As object orientation was adopted for programming languages, extension to OO-nets inspired from object-oriented programming is a natural flow. This article presents state-of-the-art on OO-nets.
We study the complexity of the reachability problem for a new subclass of Petri nets called simple-circuit Petri nets, which properly contains several well known subclasses such as conflict-free, BPP, normal Petri nets and more. A new decomposition approach is applied to developing an integer linear programming formulation for characterizing the reachability sets of such Petri nets. Consequently, the reachability problem is shown to be NP-complete. The model checking problem for some temporal logics is also investigated for simple-circuit Petri nets.
Shingo YAMAGUCHI Akira MISHIMA Qi-Wei GE Minoru TANAKA
This paper proposes a new change type for dynamic change of workflows, named Selective Shift. Workflow technology is being introduced in many companies. Workflows are business processes that allow for computerized support. The goal of workflow technology is to process workflow instances, called cases, as efficiently as possible. Companies need to change their workflows in order to adapt them to various requirements. Dynamic change is to change workflows having running cases. The most important issue in dynamic change is how running cases should be handled. Ellis et al. and Sadiq et al. have proposed change types that prescribe how to handle running cases. Their change types handle running cases collectively. If a change type can handle running cases separately, the change type would be more flexible and efficient than the conventional change types. However, there is no any change type that can handle running cases separately. Selective Shift to be proposed can handle running cases separately. We first present the concept and definition of Selective Shift. Then we give a method to handle running cases separately. Furthermore we give methods to handle running cases so that dynamic change becomes most efficient on one evaluation measure, called change time. Finally we compare Selective Shift with the conventional change types on change time by using 270 examples of dynamic change.
Akihiro TAGUCHI Atsushi IRIBOSHI Satoshi TAOKA Toshimasa WATANABE
A siphon-trap(ST) of a Petri net N = (P,T,E,α,β) is defined as a set S of places such that, for any transition t, there is an edge from t to a place of S if and only if there is an edge from a place of S to t. A P-invariant is a |P|-dimensional vector Y with YtA = for the place-transition incidence matrix A of N. The Fourier-Motzkin method is well-known for computing all such invariants. This method, however, has a critical deficiency such that, even if a given Perti net N has any invariant, it is likely that no invariants are output because of memory overflow in storing intermediary vectors as candidates for invariants. In this paper, we propose an algorithm STFM_N for computing minimal-support nonnegative integer invariants: it tries to decrease the number of such candidate vectors in order to overcome this deficiency, by restricting computation of invariants to siphon-traps. It is shown, through experimental results, that STFM_N has high possibility of finding, if any, more minimal-support nonnegative integer invariants than any existing algorithm.
Wook SHIN Jeong-Gun LEE Hong Kook KIM Kouichi SAKURAI
This paper presents the Coloured Petri Net modeling for security analysis of the Extended Role Based Access Control systems.
Akira MURAYA Tadashi MATSUMOTO Seiichiro MORO Haruo HASEGAWA
For fixed initial and destination states (i.e., markings), M0 and Md, there exist generally infinite firing count vectors in a Petri net. In this letter, it is shown that all fundamental particular solutions as well as all minimal T-invariants w.r.t. firing count vectors are needed to express an arbitrary firing count vector for the fixed M0 and Md. An algorithm for finding a special firing count vector which is expressed by using the only one specified fundamental particular solution is also given.
Sachie FUJITA Mika MATSUI Hiroshi MATSUNO Satoru MIYANO
Through many researches on modeling and analyzing biological pathways, Petri net has recognized as a promising method for representing biological pathways. Recently, Matsuno et al. (2003) introduced hybrid functional Petri net (HFPN) for giving more intuitive and natural biological pathway modeling method than existing Petri nets. They also developed Genomic Object Net (GON) which employs the HFPN as a basic architecture. Many kinds of biological pathways have been modeled with the HFPN and simulated by the GON. This paper gives a new HFPN model of "cell cycle of fission yeast" with giving six basic HFPN components of typical biological reactions, and demonstrating the method how biological pathways can be modeled with these HFPN components. Simulation results by GON suggest a new hypothesis which will help biologist for performing further experiments.
Shingo YAMAGUCHI Keisuke KUNIYOSHI Qi-Wei GE Minoru TANAKA
This paper proposes methods of computing maximum throughput for Petri nets that model workflows including resources, called WF-nets with resources. We first propose the formal definitions of WF-nets with resources and their subclasses: marked graph/state machine WF-nets with conflict-free resources (CF-Res-MG/SMWF-nets). We also show several properties of CF-Res-MG/SMWF-nets. Next we give the methods of computing maximum throughput for CF-Res-MG/SMWF-nets under condition that all tokens have to be processed in the order of First-In First-Out (FIFO). Concretely, for CF-Res-MGWF-nets, on the basis of Ramamoorthy's method of computing cycle time, we give an algorithm of computing maximum throughput under the FIFO condition. For CF-Res-SMWF-nets, there is not any method of computing maximum throughput under the FIFO condition. So we are the first to give an algorithm of computing maximum throughput for CF-Res-SMWF-nets under the FIFO condition. Finally we show an example of computing maximum throughput by using our method.
This paper addresses the scheduling problem of a class of automated manufacturing systems with multiple resource requests. In the automated manufacturing system model, a set of jobs is to be processed and each job requires a sequence of operations. Each operation may need more than one resource type and multiple identical units with the same resource type. Upon the completion of an operation, resources needed in the next operation of the same job cannot be released and the remaining resources cannot be released until the start of the next operation. The scheduling problem is formulated by Timed Petri nets model under which the scheduling goal consists in sequencing the transition firing sequence in order to avoid the deadlock situation and to minimize the makespan. In the proposed genetic algorithm with deadlock-free constraint, Petri net transition sequence is coded and a deadlock detection method based on D-siphon technology is proposed to reschedule the sequence of transitions. The enabled transitions should be fired as early as possible and thus the quality of solutions can be improved. In the fitness computation procedure, a penalty item for the infeasible solution is involved to prevent the search process from converging to the infeasible solution. The method proposed in this paper can get a feasible scheduling strategy as well as enable the system to achieve good performance. Numerical results presented in the paper show the efficiency of the proposed algorithm.
Tomoyuki YAJIMA Takashi ITO Susumu HASHIZUME Hidekazu KURIMOTO Katsuaki ONOGI
A batch process is a typical concurrent system in which multiple interacting tasks are carried out in parallel on several batches at the same time. A major difficulty in designing a batch control system is the lack of modeling techniques. This paper aims at developing a method of constructing batch control system models in a hierarchical manner and operating batch processes using the constructed models. For this purpose, it first defines process and plant specifications described by partial languages, next presents a procedure for constructing hierarchical Petri net based models, and states the verification of models based on reachability analysis. It also discusses the detection of faults and conflicts in batch processes based on place-invariant analysis.
In databases based on a multi-aspects object data model whcih enables multiple aspects of a real-world entity to be represented and to be acquired/lost dynamically, Object Migration (OM) updating membership relationships between an object and classes occurs, as the properties of the object evolve in its lifetime. We have proposed an OM behavior modeling framework using Colored Petri Nets (CPN) to analyze OM behavior. Based on the proposed framework, this paper presents a technique for constructing OM behavior models from OM constraint descriptions and class schemas as its input. The presented technique makes it easy to construct consistent and complete OM behavior models, since OM constraints are described in a simple, modular, and declarative form.
Tomoya KITAI Yusuke OGURO Tomohiro YONEDA Eric MERCER Chris MYERS
Using a level oriented model for verification of asynchronous circuits helps users to easily construct formal models with high readability or to naturally model data-path circuits. On the other hand, in order to use such a model for larger circuit, some technique to avoid the state explosion problem is essential. This paper first defines a level oriented formal model based on time Petri nets, and then proposes a partial order reduction algorithm that prunes unnecessary state generation while guaranteeing the correctness of the verification.
The paper develops the transformation rules in order to use the Stochastic Petri Net model to evaluate the performance of various task scheduling algorithms. The transformation rules are applied to DFRN scheduling algorithm to investigate its effectiveness. The performance comparison reveals that the proposed approach provides very accurate evaluation for the scheduling algorithm when the Communication to Computation Ratio value is small.
Tadashi MATSUMOTO Maki TAKATA Seiichiro MORO
Finding a nonnegative integer solution x for Ax = b (A Zmn, b Zm1) in Petri nets is NP-complete. Being NP-complete, even algorithms with theoretically bad worst case and with average complexity can be useful for a special class of problems, hence deserve investigation. Then a Grobner basis approach to integer programming problems was proposed in 1991 and some symbolic computation systems became to have useful tools for ideals, varieties, and algorithms for algebraic geometry. In this letter, Grobner basis approach is applied to three typical problems with respect to state equation in P/T Petri nets. In other words, after Grobner bases are derived by the tool Maple 7, we consider how to derive the T-invariants and particular solutions of the Petri nets by using them in this letter.
Yih-Kai LIN Cheng-Hong LI Hsu-Chun YEN
The forbidden state problem is to synthesize a control policy for preventing a Petri net from reaching any state in its forbidden set. In this paper, we address a liveness preserving version of the forbidden state problem for lossy Petri nets. During the process of keeping Petri nets out of the set of their forbidden states, a control policy does not disable a live marking. We present a method to solve the above problem based on fixed point computations. We show that for lossy Petri nets, the problem is decidable. From a practical viewpoint, the problem associated with our fixed point approach is 'state explosion. ' In order to overcome this problem, we propose a symbolic approach, which uses Boolean functions for implicitly representing the set of states. We use Boolean functions for representing reachable markings. Thus OBDDs, compact representations of Boolean functions, can reduce the time and space involved in solving the forbidden state problem described in this paper.
Shingo YAMAGUCHI Akira MISHIMA Qi-Wei GE Minoru TANAKA
This paper discusses formal modeling and performance evaluation for a type of dynamic change of workflow, called Migrate. Workflow means the flow of work and is designed to process similar instances, called cases. Companies need to continuously refine their current workflow in order to adapt them to various requirements. The change of a current workflow is called dynamic change of the workflow. Before changing a workflow, there exist cases in the workflow. If these cases are ignored or fall into deadlock, the changed workflow would become inconsistent. Since Ellis et al. proposed three change types, Flush, Abort, and Synthetic Cut-Over that keep consistency of workflows in 1995, various change types have been proposed, in which there is a promising change type called Migrate that is proposed by Sadiq et al. Sadiq et al. proposed the concept of Migrate, but did not give a formal model of Migrate. Meanwhile, we have proposed a measure, called change time, in order to evaluate dynamic change of workflows, and used this measure to evaluate the performance on change time for Ellis et al. 's three change types. However, the performance evaluation on change time for Migrate has not been done. In this paper, we first give a Petri-nets-based model of Migrate. Then we present a method of computing change time based on the net model. Finally, we apply the method to 270 examples and show the comparison results between Migrate and Ellis et al. 's three change types.
Satoshi TAOKA Katsushi TAKANO Toshimasa WATANABE
A siphon-trap of a Petri net N is defined as a place set S with